;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Mdriver.lisp")
(require "Mavltree.lisp")
(require "Mformulas.lisp")
(require "Mrng.lisp")

(link Rdriver
  (import)      
  (export Idriver)
  (Mformulas Mrng Mavltree Mdriver)
)
  
(invoke Rdriver)